Nuprl Lemma : m-sys-sub-join-list
0,22
postcript
pdf
A
:Dsys,
L
:System List. (
A
,
B
L
.
A
||
B
)
(
A
L
)
A
(
L
)
latex
Definitions
True
,
T
,
x
L
.
P
(
x
)
,
Feasible(
M
)
,
x
:
A
.
B
(
x
)
,
l
[
i
]
,
A
&
B
,
,
A
B
,
A
,
False
,
||
as
||
,
(
x
l
)
,
S
T
,
(
x
,
y
L
.
P
(
x
;
y
))
,
x
,
y
.
t
(
x
;
y
)
,
Prop
,
A
||
B
,
MsgA
,
Id
,
System
,
Dsys
,
P
Q
,
{
T
}
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
t
T
,
D1
D2
Lemmas
m-sys-join-list-property
,
dsys
wf
,
msystem
wf
,
m-sys-compatible
wf
,
pairwise
wf
,
l
member
wf
,
select
wf
,
length
wf1
,
ma-feasible
wf
,
Id
wf
,
msga
wf
origin
A:Dsys, L:System List. (A,B
L.A || B) 
(A L) A 
(L) A:Dsys, L:System List. (A,BL.A || B) (A L) A (L) 
TxL. P(x)
x:A. B(x)
B
A l) Tx,yL.P(x;y))
x,y. t(x;y) Qx:A. B(x) T D2